Nuprl Lemma : inr_eq_bfalse
4,23
postcript
pdf
x
:Top. inr(
x
) = false
Decision
latex
Definitions
Decision
,
false
,
x
:
A
.
B
(
x
)
,
t
T
,
Top
Lemmas
top
wf
origin
x:Top. inr(x) = false
Decision x:Top. inr(x) = false Decision x:A. B(x) T